(set-option :rewriter.flat false)
(set-option :model_validate true)
(declare-fun a () Int)
(declare-fun b (Int) Bool)
(declare-fun c (Int) Bool)
(push)
(assert (or (or (not (b a)) (not (c a))) (c a)))
(assert (c (- a 1)))
(assert (= (c 0) (b 0)))
(assert (b (mod a (- 1))))
(check-sat)